T,A:Type, f:(AT), l:IdLnk.
normal-type{i:l}
normal-type(A)
 normal-type{i:l}
 normal-type(T)
 (send_onceR{done:ut2, tg:ut2, b:ut2, done1:ut2}(T; A; f; l)  es_realizer{i:l}) 

latex

Definitions

top, t.2, fpf-ap(f; eq; x), tt, eq_atom{$n:n}(x; y), atom2-deq, eqof(d), bor(p; q), t.1, Y, reduce(f; k; as), deq-member(eq; x; L), fpf-dom(eq; x; f), if b then t else f fi , id-deq, fpf-cap(f; eq; x; z), x. t(x), decl-type{i:l}(ds; x), mkid{$x:ut2}, fpf-single(x; v), send_onceR{$done:ut2, $tg:ut2, $b:ut2, $done1:ut2}(T; A; f; l), t  T, P  Q, IdLnk, x:A. B(x), x(s), decl-state(ds), normal-type{i:l}(T), prop{i:l}

Lemmas

normal-type wf, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, Id wf, fpf-single wf, Rsends wf, onceR wf, Rlist wf